| Model: | embedded v.1 (CTMC) |
| Parameter(s) | MAX_COUNT = 8, T = 12 |
| Property: | actuators (prob-reach) |
mcsta/modest mcsta embedded.jani -E MAX_COUNT=8,T=12 --props actuators -O out.txt Minimal --unsafe --es -S Memory --no-partial-results --p0 --p1
| Walltime: | 7.284163236618042s |
| Return code: | 0 |
| Note(s): | The tool result '646935642857007/6250000000000000' is tagged as incorrect. The reference result is '2486339329126654286603009697501669410565922080647235572297420531003436740865701642894224651957236979415804844019970070797212838741320749871087696043790430488516768144231337033817746564261751745074561347394006816495027017797689319547300488225074500148562849173672852142305219348461967484204844049064729196699735928014471258755257981315981437194941990940151801223037104684834501918219518509576147895594521550143080313306069328271572867233516691965651482621705351476665971739605138196440899155147689763504549588268208121401875264463514032072760483012146809591389917819090345027584564812047944749664670576370371539376963526238191240909958985452275278006429583432435031807238331342878089585624527146895090748546393263058273883548791148930403418281798548198424839109773636808627978181634014955673865189747661646872651996258392552936446048778850218123619968642035042613279480618036150872134108049644406926052409061681799637826350380022669199996003596956454782552145333056157894145489486150540020412367389756815095367155100979032989577219964876141639524244527608740339422128257119204903748534580255367130745069830155822896692205418889181867570399342666796568670310583910515081237965368477709014032538181219194690388788147910806457016503932544044361342482618424045300689342156932654513810653232/23611139712102051230917389163705830960031855919193061353466918264830083378326191986369644719731733927229539492600419384037259194731474764121283541927110582338954972260482489069672524784993784262550354865456872177586787640220120819688039079785300002792915291730955593483931646644219725546280035297145057925920216590907280123192615618204899469159482885775117640880607396241557854775904114044868093404127365731780383766098536743365431606149805147123738769862714193052746662633506746823832901275751745965930188386773348462353851130634494111719846304545619011283033383773694078253680336971342463788449790335853827682934039541430969389834393278233712786556823508225268957600063594542555015850051657407051988438160129534133247921531327619001040045086238243881240503946765414870850573700427770606192511529412103367398696559809991483002140786128316014280845971470100880405232693440182197432483126227685144563355464988202359315240457890538240804613319209327258473954661426136227180487183808347011148390279684571713981594509718194717843432940624635810976882203361528885015337153218704100617865345448218447207127579308191723103792137390005496384380796220104269395092237919302086773300230575431863081466614429004067089423894856968938002028941688162575178715549796054402371237245066557533118053584375' (approx. 0.1053036557931282) which means a relative error of '0.01703599863172215' which is larger than the goal precision '0.001'. |
| Relative Error: | 0.01703599863172215 |
embedded.jani:model: info: embedded is a CTMC model.
embedded.jani: info: Need 16 bytes per state.
embedded.jani: info: Explored 5820 states for MAX_COUNT=8, T=12.0.
Peak memory usage: 53 MB
Analysis results for embedded.jani
Experiment MAX_COUNT=8, T=12.0
+ State space exploration
State size: 16 bytes
States: 5820
Transitions: 5820
Branches: 16788
Rate: 85588 states/s
Time: 0.1 s
+ Property actuators
Probability: 0.10350970285712112
Bounds: [0.10350970285712112, 1]
Time: 6.7 s
+ Precomputations
Min. prob. 0 states: 4512
Time for min. prob. 0 states: 0.0 s
Min. prob. 1 states: 180
Time for min. prob. 1 states: 0.0 s
+ Essential states
Iterations: 1
Essential states: 1130
Transitions: 1130
Branches: 7386
Time: 0.0 s
+ Value iteration
Final error: 9.999901531850148E-07
Iterations: 94800
Time: 6.7 s
Exported results to file "/out.txt".
The Modest Toolset (www.modestchecker.net), version v3.1.42-gb5e9d523c.